Inference at * 1 
Iof proof for Lemma strict part irrefl:



1. T : Type
2. R : TT
3. a : T
4. b : T
5. R(a,b)
6. R(b,a)
7. a = b
  False 

latex

 by ((OnHyps [5;6] (HypSubst 7)) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n
C),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions	t  T, x(s1,s2), P  Q, x:A. B(x), False, A,
Lemmas	not wf